COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source file
C00006 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source file;
.at "!f" ⊂"%Af%*"⊃
.at "!y" ⊂"%Ay%*"⊃
.cb
Derived Functions
.break
	A derived function ⊗f' of ⊗f contains a computation sequence of ⊗f in its
arguments and values.  We speculate that proving assertions about derived
functions may be easier because more information is kept.  Induction on a
derived function may sometimes correspond to something like course-of-values
induction on the original.  We would like to say "the derived function"
instead of "a derived function" and "the computation sequence" instead of
"a computation sequence", but a single preferred notion has not yet become
apparent.  Note also that the derived function will depend on the way the
function is described and not just on the argument-value pairing.

	Derived functions are presumably related to their originals by something
like the homomorphism theorem and are therefore equi-convergent.
[The homomorphism theorem is %2∀ff'. [(!f %8o%2 f = f' %8o%2 !y) ⊃ (!f %8o%2
F(f) = F'(f') %8o%2 !y)] ⊃ (!f %8o%2 Y(F) = Y(F') %8o%2 !y)]%1.

	Here are some examples of functions and derived functions:
.begin nofill

#. 	%2f x ← qif p x qthen x qelse f h x

	f' u ← qif p qa u qthen u qelse f'(h qa u . u)

	f''(x,u) ← qif p x qthen u qelse f''(h x, x . u)

#.	f x ← qif x > 100 qthen x-10 qelse f f (x + 11)

	f'(x,v) ← qif x > 100 qthen (x - 10) . v qelse [λ w . f'(qa w, w)][f'(x + 11,%8 %2(x%8 %2+%8 %211)%8 %2.%8 %2v)]

#.	flat[x,u] ← qif qat x qthen x . u qelse flat[qa x, flat[qd x, u]]

	flat'[x,u,v] ← qif qat x qthen [x . u] . v qelse
	     [λ z . flat'[qa x, qa z, qa x . dz]] [flat'[qd x, u, qd x . v]]

	flat''[x,u,v] ← qif qat x qthen (x . u) . v qelse
	      [λ z flat''[qa x, qa z, <qa x qa z> . qd z]] [flat''[qd x, u, <qd x u> . v]]

#.	flatten x ← qif qat x qthen <x> qelse flatten qa x * flatten qd x

	flatten'[x,v] ← qif qat x qthen <x> . v qelse
	        α{flatten'[qa x, qa x . v]} [λ z . α{flatten'[qd x, qd x . qd z]} [λ w [qa z * q w] . qd w]
.end